0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳10 CpxRNTS
↳11 InliningProof (UPPER BOUND(ID), 0 ms)
↳12 CpxRNTS
↳13 SimplificationProof (BOTH BOUNDS(ID, ID), 3 ms)
↳14 CpxRNTS
↳15 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CpxRNTS
↳17 IntTrsBoundProof (UPPER BOUND(ID), 101 ms)
↳18 CpxRNTS
↳19 IntTrsBoundProof (UPPER BOUND(ID), 12 ms)
↳20 CpxRNTS
↳21 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳22 CpxRNTS
↳23 IntTrsBoundProof (UPPER BOUND(ID), 173 ms)
↳24 CpxRNTS
↳25 IntTrsBoundProof (UPPER BOUND(ID), 75 ms)
↳26 CpxRNTS
↳27 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳28 CpxRNTS
↳29 IntTrsBoundProof (UPPER BOUND(ID), 343 ms)
↳30 CpxRNTS
↳31 IntTrsBoundProof (UPPER BOUND(ID), 140 ms)
↳32 CpxRNTS
↳33 FinalProof (⇔, 0 ms)
↳34 BOUNDS(1, n^1)
and(tt, X) → activate(X)
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))
activate(X) → X
and(tt, X) → activate(X) [1]
plus(N, 0) → N [1]
plus(N, s(M)) → s(plus(N, M)) [1]
activate(X) → X [1]
and(tt, X) → activate(X) [1]
plus(N, 0) → N [1]
plus(N, s(M)) → s(plus(N, M)) [1]
activate(X) → X [1]
and :: tt → and:activate → and:activate tt :: tt activate :: and:activate → and:activate plus :: 0:s → 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s |
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
and
plus
activate
const
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
tt => 0
0 => 0
const => 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
and(z, z') -{ 1 }→ activate(X) :|: z' = X, X >= 0, z = 0
plus(z, z') -{ 1 }→ N :|: z = N, z' = 0, N >= 0
plus(z, z') -{ 1 }→ 1 + plus(N, M) :|: z' = 1 + M, z = N, M >= 0, N >= 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ X :|: X >= 0, z = X
and(z, z') -{ 2 }→ X' :|: z' = X, X >= 0, z = 0, X' >= 0, X = X'
plus(z, z') -{ 1 }→ N :|: z = N, z' = 0, N >= 0
plus(z, z') -{ 1 }→ 1 + plus(N, M) :|: z' = 1 + M, z = N, M >= 0, N >= 0
activate(z) -{ 1 }→ z :|: z >= 0
and(z, z') -{ 2 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0
{ activate } { and } { plus } |
activate(z) -{ 1 }→ z :|: z >= 0
and(z, z') -{ 2 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0
activate(z) -{ 1 }→ z :|: z >= 0
and(z, z') -{ 2 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0
activate: runtime: ?, size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
and(z, z') -{ 2 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
and(z, z') -{ 2 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
and(z, z') -{ 2 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] and: runtime: ?, size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
and(z, z') -{ 2 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [2], size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
and(z, z') -{ 2 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [2], size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
and(z, z') -{ 2 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [2], size: O(n1) [z'] plus: runtime: ?, size: O(n1) [z + z'] |
activate(z) -{ 1 }→ z :|: z >= 0
and(z, z') -{ 2 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [2], size: O(n1) [z'] plus: runtime: O(n1) [1 + z'], size: O(n1) [z + z'] |